FDL - Nuprl Lemma : rcv-it-of-snd-it

Nuprl Lemma : rcv-it-of-snd-it

es:ES, ff:FIFO, p:(E

), i, j:ff.C, e:E.
(

i:ff.C, e:E. Dec(ff.R(i,e)))

[e: i

p

j]

[ff.Receiver(i,j,e): j

p

i]

Definitions x:A. B(x), , P Q, [e: i p j], t T, P & Q, x:A. B(x), T, True, [e: i p j], SqStable(P)

Lemmas snd-it wf, fifoC wf, es-E wf, decidable wf, fifoR wf, FIFO wf, event system wf, fifoReceiver-properties, fifoS wf, fifoReceiver wf, fifoSender wf, sq stable from decidable